package test
class WeakEqTest2 extends EqTester {
  override def beforeAll {
    super.beforeAll()
    loadBasicAgents()
  }

  test("A and tau.A are bi-similarly equivalent") {
    weakAssert("(tau.A, A)", true)
    weakAssert("(tau.A', A')", true)
    weakAssert("(tau.A', A)", true)
    weakAssert("(tau.A, A')", true)
    weakAssert("(tau.A, B)", false)
    weakAssert("(tau.A', B')", false)
    weakAssert("(tau.A', B)", false)
    weakAssert("(tau.A, B')", false)
    weakAssert("(tau.A, C)", false)
    weakAssert("(tau.A', C')", false)
    weakAssert("(tau.A', C)", false)
    weakAssert("(tau.A, C')", false)
    weakAssert("(tau.A, D)", false)
    weakAssert("(tau.A', D')", false)
    weakAssert("(tau.A', D)", false)
    weakAssert("(tau.A, D')", false)
    weakAssert("(tau.A, E)", false)
    weakAssert("(tau.A', E')", false)
    weakAssert("(tau.A', E)", false)
    weakAssert("(tau.A, E')", false)
  }

  test("B and tau.B are bi-similarly equivalent") {
    weakAssert("(tau.B, A)", false)
    weakAssert("(tau.B', A')", false)
    weakAssert("(tau.B', A)", false)
    weakAssert("(tau.B, A')", false)
    weakAssert("(tau.B, B)", true)
    weakAssert("(tau.B', B')", true)
    weakAssert("(tau.B', B)", true)
    weakAssert("(tau.B, B')", true)
    weakAssert("(tau.B, C)", false)
    weakAssert("(tau.B', C')", false)
    weakAssert("(tau.B', C)", false)
    weakAssert("(tau.B, C')", false)
    weakAssert("(tau.B, D)", false)
    weakAssert("(tau.B', D')", false)
    weakAssert("(tau.B', D)", false)
    weakAssert("(tau.B, D')", false)
    weakAssert("(tau.B, E)", false)
    weakAssert("(tau.B', E')", false)
    weakAssert("(tau.B', E)", false)
    weakAssert("(tau.B, E')", false)
  }

  test("C and tau.C are bi-similarly equivalent") {
    weakAssert("(tau.C, A)", false)
    weakAssert("(tau.C', A')", false)
    weakAssert("(tau.C', A)", false)
    weakAssert("(tau.C, A')", false)
    weakAssert("(tau.C, B)", false)
    weakAssert("(tau.C', B')", false)
    weakAssert("(tau.C', B)", false)
    weakAssert("(tau.C, B')", false)
    weakAssert("(tau.C, C)", true)
    weakAssert("(tau.C', C')", true)
    weakAssert("(tau.C', C)", true)
    weakAssert("(tau.C, C')", true)
    weakAssert("(tau.C, D)", false)
    weakAssert("(tau.C', D')", false)
    weakAssert("(tau.C', D)", false)
    weakAssert("(tau.C, D')", false)
    weakAssert("(tau.C, E)", false)
    weakAssert("(tau.C', E')", false)
    weakAssert("(tau.C', E)", false)
    weakAssert("(tau.C, E')", false)
  }

  test("D and tau.D are bi-similarly equivalent") {
    weakAssert("(tau.D, A)", false)
    weakAssert("(tau.D', A')", false)
    weakAssert("(tau.D', A)", false)
    weakAssert("(tau.D, A')", false)
    weakAssert("(tau.D, B)", false)
    weakAssert("(tau.D', B')", false)
    weakAssert("(tau.D', B)", false)
    weakAssert("(tau.D, B')", false)
    weakAssert("(tau.D, C)", false)
    weakAssert("(tau.D', C')", false)
    weakAssert("(tau.D', C)", false)
    weakAssert("(tau.D, C')", false)
    weakAssert("(tau.D, D)", true)
    weakAssert("(tau.D', D')", true)
    weakAssert("(tau.D', D)", true)
    weakAssert("(tau.D, D')", true)
    weakAssert("(tau.D, E)", false)
    weakAssert("(tau.D', E')", false)
    weakAssert("(tau.D', E)", false)
    weakAssert("(tau.D, E')", false)
  }

  test("E and tau.E are bi-similarly equivalent") {
    weakAssert("(tau.E, A)", false)
    weakAssert("(tau.E', A')", false)
    weakAssert("(tau.E', A)", false)
    weakAssert("(tau.E, A')", false)
    weakAssert("(tau.E, B)", false)
    weakAssert("(tau.E', B')", false)
    weakAssert("(tau.E', B)", false)
    weakAssert("(tau.E, B')", false)
    weakAssert("(tau.E, C)", false)
    weakAssert("(tau.E', C')", false)
    weakAssert("(tau.E', C)", false)
    weakAssert("(tau.E, C')", false)
    weakAssert("(tau.E, D)", false)
    weakAssert("(tau.E', D')", false)
    weakAssert("(tau.E', D)", false)
    weakAssert("(tau.E, D')", false)
    weakAssert("(tau.E, E)", true)
    weakAssert("(tau.E', E')", true)
    weakAssert("(tau.E', E)", true)
    weakAssert("(tau.E, E')", true)
  }

}
